Add Kani proof harnesses establishing the memory safety of all 12
  safe-functions-with-unsafe-bodies in core::num::flt2dec: the 6 formatting
  entry points (flt2dec/mod.rs) and the 6 Grisu/Dragon strategy functions
  (flt2dec/strategy/{grisu,dragon}.rs).

  Each unsafe block (MaybeUninit::assume_init_* and slice indexing) is proven
  to touch only initialized, in-bounds memory. The bignum/Fp arithmetic is
  abstracted via sound stubbing -- buffer safety is independent of the numeric
  values, and value inspection (cmp/is_zero) is made nondeterministic so all
  control-flow paths are explored.

  The shortest-mode functions (grisu::format_shortest_opt,
  dragon::format_shortest)
  have an implicit loop bound; their digit index is bounded by the Grisu/Loitsch
  digit-count theorem (a 53-bit-precision f64 has <= MAX_SIG_DIGITS = 17
  significant decimal digits), cited as a cfg(kani) assume because CBMC cannot
  derive it from the unwound arithmetic. The harnesses use the tight decode()
  precondition (the functions are internal and only ever receive a decode()
  result for a real f64), which is what makes that assume sound.

  All added annotations are cfg(kani) verification-only and compile out of normal
  builds. Harnesses require -C debug-assertions=off.

Signed-off-by: Onyeka Obi <softwareengineerasaservant@isurvivable.cv>

…ition-2 OOM)

  - Remove concrete dragon::check_format_exact: full unstubbed bignum (unwind 50)
    exhausted CBMC memory in the verify-std partition (ran ~6h, cancelled).
    format_exact buffer safety is already proven by check_format_exact_stub.
  - Run autoharness with debug-assertions off: the flt2dec harnesses stub the
    bignum/Fp arithmetic, making std debug_assert! digit-correctness checks
    (d<10, mant<scale) unprovable. Those are not memory-safety properties and are
    already dead in the verify-std job (--prove-safety-only). Keeps the two jobs
    consistent; monotonic (only removes checks).

Signed-off-by: Onyeka Obi <softwareengineerasaservant@isurvivable.cv>

  global flag

  e104d40 set RUSTFLAGS: -C debug-assertions=off on the autoharness job. That
  also disables overflow-checks, which made two unrelated heavy harnesses
  (slice align_to_u128, slice char check_pre_dec_end) blow past the 10-minute
  CBMC timeout (~6s with the checks on). Revert that env.

  The three Grisu digit-loop harnesses (check_format_shortest_opt,
  check_format_shortest_opt_norw, check_format_exact_opt) run the real digit
  loop while havoc-stubbing Fp::mul/cached_power, which makes std's
  value-dependent debug_assert! digit-correctness checks (q < 10,
  ten_kappa == 1) unprovable. They pass only with debug-assertions off, but
  verify-std runs with them on (run-kani.sh uses neither --prove-safety-only
  nor that flag), so check_format_shortest_opt_norw failed partition 2. There
  is no per-harness debug-assertions toggle and disabling it globally times out
  other harnesses, so drop these three.

  The remaining ten harnesses (wholesale-stub check_format_exact /
  check_format_shortest, the two dragon stubs, and the six string-formatting
  harnesses) prove buffer/init safety of the public flt2dec entry points and
  the dragon fallback, and all verify with debug-assertions on.

Signed-off-by: Onyeka Obi <softwareengineerasaservant@isurvivable.cv>